\chapter{K framework overview}
In 2003, Grigore Ro\c{s}u, Assistant Professor at University of Illinois at Urbana-Champaign, introduced K as a technique in his programming languages course. K technique assumed to write what is today a K definition and then translate it into Maude \cite{maude} by hand in order to execute it. Later, this process has been automated and now there is a prototype of K, called K-Maude, which uses Maude Rewriting Engine as a backend.
As described in \cite{jlap2010}, K is an executable semantic framework in which programming languages, calculi, as well as type systems or formal analysis tools can be defined, making use of {\it configurations}, {\it computations} and {\it rules}.\\
In K definitions a {\it configuration} is represented by a {\it nested cell} structure. {\it Configurations} organize the system/program state in units called {\it cells}, which are labeled and can be nested. {\it Computations} carry computational meaning as special nested list structures sequentializing computational tasks, such as fragments of program; in particular, computations extend the original language or calculus syntax. K (rewrite) {\it rules} generalize conventional rewrite rules by making explicit which parts of the term they read, write, or do not care about.\\
\begin{minipage}{.8\textwidth}
In order to familiarize you with K, we will make a description of the K definition of a very simple imperative language called IMP. K allows users to split their definitions into modules which usually separates the syntax by the semantics, but this is not a restriction. Basic definition of IMP has three modules: IMP-SYNTAX, IMP-SEMANTICS and IMP. The first module contains the syntax of IMP which is given using BNF (Backus-Naur Form or Backus Normal Form) notation technique for context-free grammars. As we can see in Figure \ref{imp:syntax} our language has two types of expressions:
\item arithmetic expressions defined by non-terminal {\it AExp} which is a K builtin identifier ({\it Id}) or a K builtin integer ({\it Int}). Also, we can have two operations on arithmetic expressions: {\it +} and {\it /}.
\item boolean expressions defined using non-terminal {\it BExp} which has type {\it Bool} and operations $\leq$ (applied on two arithmetic expressions), {\it and} and {\it not} (applied on {\it BExp}).
Syntax also contains the instruction set used in IMP programs. The non-terminal {\it Stmt} is used to generate the following instructions (in this order):
\item assignment of variables with arithmetic expressions
An IMP program contains a section for variable declarations and then the list of statements to be executed. Non-terminal {\it IdList} specifies that variables should be declared all at once after {\it var} keyword, separated by ','. 
On the right hand side of each operator declaration a K attribute is specified. For IMP, only variations of {\it strict} attribute are used. They have the following meaning:
\item {\bf [strict]} - specifies that all specified arguments for the given operator must be evaluated before evaluating the construct itself. For example, {\bf +}, {\bf /} and {\bf not} have strictness attribute because we want to evaluate the arithmetic expressions from left and right first and then evaluate the actual operation, or, the boolean expression before applying {\bf not} to it.
\item {\bf [strict(i)]} - restricts the attribute {\bf [strict]} to argument on position {\bf i}. For {\bf and} operator or {\it if-then-else} statement we want to evaluate the first argument. In first case, it is enough to evaluate first argument in order to evaluate the {\bf and} operation and in the second case, we must evaluate first the condition for {\it if-then-else} and then we evaluate the statement to content of the correct branch. For assignment, we use {\bf [strict(2)]} because we must evaluate the value (arithmetic expression) first and then assign it to variable name.
\item{\bf [seqstrict]} - is like {\bf [strict]} but each argument is fully processed before moving to the next one. This is useful when we have to specify how {\it AExp $\leq$ AExp} is evaluated: evaluate second {\it AExp} after the complete evaluation of first {\it AExp}.
The most interesting part is how to give the semantics for this language in K. For this, K uses configurations and rewriting rules. A nice example of configuration for IMP can be found in \cite{jlap2010}.
The configuration is a nested cell structure which contains informations about the state of the execution of a program.  The configuration of IMP contains the following cells:
\item {\it T} - is the top cell and contains two other cells: {\it k} and {\it state}
\item {\it k} - a cell which holds a term of sort {\it K} (terms of sort K are called computations and extend the original language syntax)
\item {\it state} - a cell which holds a map from variables to integers
Actually the main idea is to keep in the configuration everything we need in order to define the semantics using rewriting rules. Intuitively, these rules will modify the configuration according to the specified semantics. Each syntactic construct has a corresponding rule. For example, $+$ operator is rewritten in $+_{Int}$ which is the built-in addition operator in K framework. Its corresponding rule says that when an addition expression is matched then rewrite it into a built-in addition operation and evaluate that expression. So, the way rules are applied is the following: when an expression from the left hand side is found on the top of the computation cell then rewrite it with the right hand side. Below is the semantics of IMP language explained:\\
K rules are very intuitive. For example, the look-up rule says that whenever in the {\it k} cell we find a variable which must be evaluated then go in {\it state} cell and get its corresponding value {\it I} and put it in {\it k}. This means that {\it I} is the result of the evaluation. Rules for {\it if-then-else} statement are applied only if the boolean condition is evaluated already to {\it true} or {\it false}. In case the condition is {\it true} the rule {\it IF-THEN-ELSE-TRUE} says that the statement should be replaced by the statements under {\it then} branch. The List\{K\} under {\it else} matches all statements which will never be executed and we do not care about them anymore. {\it WHILE-LOOP} rule uses a nice technique: unrolling the loop into an {\it if-then-else} statement and the rest of the loop. At some point the loop condition will become {\it false} and the loop will exit through {\it else} branch.\\
The definition of IMP is very simple and can be easily understood. It can serve as a very useful example for K newbies and this is the reason why it is used in teaching K. The framework offers a compiler which generates an interpreter for such a definition without any other effort than the definition itself.\\
 SIMPLE is intended to be a pedagogical language that captures the
 essence of the imperative programming paradigm, extended with several
 features often encountered in imperative programming languages.
 A program consists of a set of global variable declarations and
 function definitions.  Like in C, function definitions cannot be
 nested and each program must have one function called \texttt{main},
 which is invoked when the program is executed.  To make it more
 interesting and to highlight some of \K's strengths, SIMPLE includes
 the following features in addition to the conventional imperative
 expression and statement constructs:
 \item Multidimensional arrays and array references.  An array evaluates
 to an array reference, which is a special value holding a location where
 the elements of the array start together with the size of the array;
 the elements of the array can be array references themselves when the
 array is multi-dimensional.  Array references are ordinary values, so
 they can be assigned to variables and passed/received by functions.
 \item Functions and function references.  Functions can have zero or
 more parameters and can return abruptly using a \texttt{return} statement.
 SIMPLE is call-by-value with static scoping.  Function names evaluate to
 function references, which hereby become ordinary values in the language,
 same like the array references.
 \item Blocks with locals.  SIMPLE allows variables to be declared
 anywhere, their scope being the most nested block containing them.
 \item Input/Output.  The expression \texttt{read()} evaluates to the
 next value in the input buffer, and the statement \texttt{write(e)}
 evaluates \texttt{e} and outputs its value to the output buffer.  The
 input and output buffers are lists of values.
 \item Exceptions.  SIMPLE has parametric exceptions (the value thrown as
 an exception can be caught and bound).
 \item Concurrency via dynamic thread creation/termination and
 synchronization.  One can spawn a thread to execute any statement.
 The spawned thread shares with its parent its environment at creation time.
 Threads can be synchronized via reentrant locks which can be acquired and
 released, as well as through rendezvous.
The full semantics of SIMPLE can be found in the Appendix. 